package at.ac.tuwien.big.forms.alloygen

import org.eclipse.emf.ecore.resource.Resource
import org.eclipse.xtext.generator.IFileSystemAccess
import org.eclipse.xtext.generator.IGenerator
import java.io.File
import at.ac.tuwien.big.forms.EntityModel
import at.ac.tuwien.big.forms.Entity
import at.ac.tuwien.big.forms.EntityModelElement
import at.ac.tuwien.big.forms.Feature
import at.ac.tuwien.big.forms.Relationship
import at.ac.tuwien.big.forms.Attribute
import at.ac.tuwien.big.forms.AttributeType

class Form2AlloyGenerator implements IGenerator {

  override doGenerate(Resource resource, IFileSystemAccess fsa) {
    var entityModel = resource.contents.get(0) as EntityModel
    var name = new File(resource.URI.toFileString).name.replace(".forms", ".als");
  
    fsa.generateFile(name,
      '''module ME14
«FOR EntityModelElement e : entityModel.entityModelElements»
«IF e instanceof Entity»
sig «(e as Entity).name» {
  «FOR Feature f : e.features»
    «IF f instanceof Relationship»
      «f.name»: 
      «IF f.lowerBound >= 0 && f.lowerBound != 1 && f.upperBound == -1» set 
      «ELSEIF f.lowerBound == 0 && f.upperBound == 1» lone 
      «ELSEIF f.lowerBound == 1 && f.upperBound == 1» one
      «ELSEIF f.lowerBound == 1 && f.upperBound == -1» some
      «ENDIF»
      «f.target.name»,
    «ELSEIF f instanceof Attribute»
      «f.name»: «(f as Attribute).type»,
    «ENDIF»
  «ENDFOR»
}
«ENDIF»  
«ENDFOR»

««««FOR EntityModelElement e : entityModel.entityModelElements»
««««IF e instanceof Entity»
«««  «FOR Feature f : e.features»
«««    «IF f instanceof Attribute»
«««      «IF (f as Attribute).type != AttributeType::INTEGER && (f as Attribute).type != AttributeType::STRING && (f as Attribute).type != AttributeType::BOOLEAN»
«««enum «(f as Attribute).type» {
«««  Yes, No
«««}
«««      «ENDIF»
«««    «ENDIF»
«««  «ENDFOR»
««««ENDIF»  
««««ENDFOR»
    
fact{
«FOR EntityModelElement e : entityModel.entityModelElements»
«IF e instanceof Entity»
«FOR Feature f : e.features»
«IF f instanceof Relationship»
«IF f.lowerBound > 0 && f.lowerBound != 1» (all z:«e.name» | #z.«f.name» >= «f.lowerBound») and
«ELSEIF f.lowerBound > 0 && f.lowerBound != 1 && f.upperBound == f.lowerBound» | #z.«f.name» = «f.lowerBound») and
«ELSEIF f.upperBound != -1 && f.upperBound != 1» (all z:«e.name» | #z.«f.name» <= «f.upperBound») and 
«ENDIF»
«IF f.opposite instanceof Feature»
(all x:«e.name» | all y:«f.target.name» | y in x.«f.name» implies x in y.«f.opposite.name») and
«ENDIF»
«ENDIF»
«ENDFOR»
«ENDIF»
«ENDFOR»
}'''
    )
  }
}